M:MsgA, x:Id, v:(M.ds(x)). M.init(x)?v  M.ds(x) 

latex

Definitions	MsgA, M.ds(x), Valtype(da;k), M.init(x)?v, left + right, Unit, P  Q, P & Q, x  dom(f), a:A fp B(a), f(x), suptype(S; T), EqDecider(T), S  T, Top, x,y:A//B(x;y), x,y. t(x;y), P  Q, qeq(r;s), tt, EquivRel(T;x,y.E(x;y)), A  B, x:A  B(x), , , x:AB(x), , f(x)?z, x. t(x), x.A(x), Id, IdDeq, Type, Void, , s = t, , b, A, b, x:A. B(x), t  T
Lemmas	assert wf, not wf, bnot wf, bool wf, id-deq wf, Id wf, fpf-cap wf, rationals wf, int nzero wf, b-union wf, btrue wf, qeq wf2, quotient wf, fpf-cap-void-subtype, deq wf, subtype rel self, fpf-ap wf, fpf-trivial-subtype-top, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, msga wf, ma-ds wf